(set_true_11 zero)
(set_true_11 obj1)
(begin-proof )
(establish_and_2 max zero)
(establish_or_7_0 max zero)
(establish_exists_8 max zero)
(establish_and_6 obj1 obj2)
(establish_or_7_1 obj1 obj2)
(establish_exists_8 obj1 obj2)
(establish_and_2 obj2 obj1)
(establish_or_7_0 obj2 obj1)
(establish_exists_8 obj2 obj1)
(establish_and_2 zero zero)
(establish_or_7_0 zero zero)
(establish_exists_8 zero zero)
(establish_forall_9_base )
(establish_forall_9_inductive zero obj1)
(establish_forall_9_inductive obj1 obj2)
(establish_forall_9_inductive obj2 max)
(prove-goal )
